ds:x:Id fp Type, da:k:Knd fp Type, k:Knd, l:IdLnk, tg:Id, n:,
f:(State(ds)Valtype(da;k)da(rcv(l,tg))?Void).
k sends on l with tag tg [s,v.f(s,v)], at marker n  msg-spec(ds;da) 

latex

Definitions	Void, Type, t  T, x:A. B(x), rcv(l,tg), KindDeq, Knd, x.A(x), x. t(x), f(x)?z, type List, Valtype(da;k), x:AB(x), State(ds), , x:AB(x), nil, f(a), x(s1,s2), car.cdr, <a,b>, msg-item(ds;da;k;l), P  Q, False, A, AB, , {x:A| B(x) }, IdLnk, 2of(t), 1of(t), k sends on l with tag tg [s,v.f(s;v)], at marker n, msg-spec(ds;da), Id, a:A fp B(a)
Lemmas	fpf wf, Id wf, fpf-single wf, pi1 wf, pi2 wf, IdLnk wf, msg-item wf, nat wf, decl-state wf, ma-valtype wf, fpf-cap wf, Knd wf, Kind-deq wf, rcv wf